Code and Notes (Week 9 Thursday)

1. Notes
2. Haskell code
3. Java code
- 3.1. Liskov substitution principle
- 3.2. Unsound covariance of arrays

These are the extra notes and code I presented in today's lecture. Many thanks to Johannes Åman Pohjola for the original.

1. Notes

Three types of polymorphism
---------------------------

- parametric polymorphism
   (abstract from specific types w/ variables ranging over types)

   [Int]
   [Float]

   append :: forall a. [a] -> [a] -> [a]
     *same* implementation regardless of a

- ad-hoc polymorphism (overloading) 
   the feature that lets you write + for both int addition
   and float addition

   1 + 2 :: Int
   3.4 + 6.7 :: Float

   a -> a -> a
     *different* implementation for Int vs Float

- subtype polymorphism
   the feature that lets you treat a Dog as an Animal in Java

    class Animal {}
    class Cat extends Animal {}
    class Dog extends Animal {}


Extending MinHS with type classes
---------------------------------

Having constraints only on the polytypes means we won't allow this:

    x :: a -> (Num a => a)

Only on the outer level, like:

    x :: Num a => a -> a 

:info Num

Here's an example of what you'd find in axiom schema set A:

    {Num Word, Num Integer, Num Int, Num Float, Num Double}


Typing Rules for Overloading
----------------------------

Pass-through of A by existing rules:

    A|Γ ⊢ e1 : τ1       A|Γ ⊢ e2 : τ2
   _______________________
     A|Γ ⊢ (e1,e2) : τ1 × τ2

Using instantiation rule to eliminate typeclass Num constraint:

     A | Γ ⊢ e : Num Int ⇒ Int      A |⊢ Num Int
    _____________________________________________ Inst
             A | Γ ⊢ e : Int

Using generalisation rule to introduce typeclass Num constraint:

         Num a, A | Γ ⊢ double : a -> a 
        _________________________________ Gen
         A | Γ ⊢ double : Num a ⇒ a -> a


Partial order
-------------

  A relation R is a partial order if:

  Transitive:

     x R y   ∧   y R z   ⇒ x R z

  Reflexive

     x R x

  Anti-symmetric:

     x R y  ∧  y R x   ⇒ x ≠ y

For subtyping:

  class Siamese extends Cat

  class Cat extends Animal
  // we would like a Siamese   to count as an Animal --> transitivity
  // reflexivity: we would like a Siamese to count as a Siamese

  // anti-symmetry: no cycles in the subclass hierarchy

2. Haskell code

module W9B where

{- Overloading -}

{-
  ghci> :t (+)
  (+) :: Num a => a -> a -> a

  (+) has type a -> a -> a
    for every type that is a member of the class Num
 -}

-- Here's a function that works for types a
-- that satisfy typeclass constraint Num a
double :: Num a => a -> a
double x = x + x

-- Let's make our own datatypes an instance of Num, too!
data Fruit = Apple | Banana
  deriving Eq
  -- deriving (Eq,Show)
  -- deriving Show
-- ^ uses Haskell's default implementation for Show's methods

-- `:info Num` will tell you typeclass Num's methods
-- and here's how you can implement them manually:
instance Num Fruit where
  _ + _ = Apple
  _ * _ = Banana
  f1 - f2 = f2
  negate f = f
  abs f = Apple
  signum f = Banana
  fromInteger _ = Apple

-- `:info Num` will tell you similarly for Show,
-- and also can implement Show's methods manually:
instance Show Fruit where
  show Apple = "Apfel"
  show Banana = "Banane"

-- Haskell will try to infer the most general type class constraints
-- my_thing :: (Eq a, Num a) => a -> Bool
my_thing x =
  x + x == x

-- You can define your own typeclass like this:
class Sized a where
  size :: a -> Int

-- Here are a few instances for it:
instance Sized Bool where
  size True = 1
  size False = 0

instance Sized Int where
  size x = x

-- Generative instance -- more on this later
-- instance Sized a => Sized [a] where
--   size xs = sum (map size xs)

-- This should work for all the above instances
doubleSize :: Sized a => a -> Int
doubleSize x = 2*size x

{- What the type class constraint
      Sized a
   means is:

    a is a type with a size function defined.

   So: why not just pass the size function
    as an extra argument?
 -}

-- Now this is parametric polymorphism.
-- The first argument is the type for dictionaries
-- of the "size" typeclass:
doubleSize' :: (a -> Int) -> a -> Int
doubleSize' size x = 2*size x

-- the dictionary for `instance Sized Bool` would look like this
sizeBool :: Bool -> Int
sizeBool True = 1
sizeBool False = 0


{- Static dispatch doesn't work for polymorphic recursion -}

-- not polymorphic recursion
data MyList a = MyNil | MyCons a (MyList a)

-- polymorphic recursion: no good for static dispatch
-- (inlining of typeclass dictionary calls), because
-- you'd need unboundedly many dictionaries...
data Thing a =
  T (Thing [a])


{- Subtyping and its interaction with constructors -}

{- For product types:
 - Assuming Int <= Float,

         (Float,Float)
        /          \
       /            \
 (Float,Int)       (Int,Float)
       \          /
        \        /  Example below
          (Int,Int)

Well this seems to be right?

    (Int,Int)  <= (Int,Float)

But why?
  -}

-- The fact that Int <= Float is represented by the following
-- coercion function existing:
coerce :: Int -> Float
coerce = undefined -- well, the specific definition doesn't matter,
                   -- but it has to exist

-- Using that coercion, we get this one:
coerceII2IF :: (Int,Int) -> (Int,Float)
coerceII2IF (i1,i2) = (i1,coerce i2)

{- and similarly, we can get the other four edges.
 - but there's no relation between (Float,Int) and (Int,Float)! -}

-- We can also get this kind of hierarchy for sum types, e.g.
coerceII2IF' :: Either Int Int -> Either Int Float
coerceII2IF' (Left n) = Left n
coerceII2IF' (Right n) = Right(coerce n)
-- and so forth.

something :: (Float -> Int) -> (Float -> Float)
something f = \x -> coerce (f x)

somethingElse :: (Float -> Int) -> (Int -> Float)
somethingElse f = \x -> coerce $ f $ coerce x


{- Coercing a function between these types:

    Int -> Int

    Int -> Float

    Float -> Int

    Float -> Float

   Between which of these can we coerce, and
   when do we apply `coerce :: Int -> Float`?
 -}

-- Contravariance
-- Originally we had Int <= Float, now we have:
-- (Float -> Int) <= (Int -> Int)
coerceFun :: (Float -> Int) -> (Int -> Int)
coerceFun f = \n -> f(coerce n)

-- Covariance
-- Originally we had Int <= Float, now we have:
-- (Int -> Int) <= (Int -> Float)
coerceFun' :: (Int -> Int) -> (Int -> Float)
coerceFun' f = \n -> coerce(f n)

{-
 Covariance:
  - the relationship between the argument type(s)
    is the same as the relationship between the composite types
 Contravariance:
  - the relationship between the argument type(s)
    is the inverse of the relationship between the composite types
 -}

3. Java code

3.1. Liskov substitution principle

This (maybe a little cheap) example is meant to illustrate the impossibility of fully complying with the Liskov substitution principle in Java.

class Animal {}

class Cat extends Animal {}

class Dog extends Animal {}

public class Liskov {
    public static void main(String [] args) {
        // This prints "class Dog"
        System.out.println((new Dog()).getClass().toString());
        // This prints "class Animal"
        System.out.println((new Animal()).getClass().toString());
        // Checkmate, Java proponents!
    }
}

3.2. Unsound covariance of arrays

The basic arrays in Java are covariant, allowing the following:

class Animal {}

class Dog extends Animal {}

class Cat extends Animal {}

public class Dog2Cat {
    public static Cat dog2cat(Dog dog) {
        Cat[] cats = new Cat[10];
        // Only possible because arrays are covariant:
        //   Wherever we have an array of Animal,
        //   we can have an array of Cat.
        // Cat <= Animal, so Cat[] <= Animal[]
        Animal[] animals = cats;
        animals[0] = dog; // bad. Is animals[0] a Cat or Dog?
        return cats[0];
    }

    public static void main(String[] args) {
        Dog dog = new Dog();
        Cat cat = dog2cat(dog);
        System.out.println("Hello world!");
    }

}

Java then added ArrayLists and made them invariant instead.

import java.util.ArrayList;

class Animal {}

class Dog extends Animal {}

class Cat extends Animal {}

public class Dog2Cat2 {
    public static Cat dog2cat(Dog dog) {
        ArrayList<Cat> cats = new ArrayList<>(10);
        // ArrayLists are invariant:
        // Cat <= Animal, but ArrayList<Cat> </= ArrayList<Animal>
        ArrayList<Animal> animals = cats; // no longer allowed
        animals.add(dog);
        return cats.get(0);
    }

    public static void main(String[] args) {
        Dog dog = new Dog();
        Cat cat = dog2cat(dog);
        System.out.println("Hello world!");
    }

}

But despite that, Amin and Tate proceeded to show that Java's (and Scala's) type systems are unsound: https://io.livecode.ch/learn/namin/unsound

Some good, as-yet unanswered questions from today's class discussion:

Would it be okay to declare an ArrayList<Animal> animals first then assign dogs and cats to its entries? (But if so, you couldn't return Dog or Cat, right?)
Are these all just pointers, and if so, is the issue that the underlying value is somehow simultaneously an ArrayList<Cat> and an ArrayList<Animal> after the assignment of animals = cats?
Alternatively, does the assignment animals = cats involve a coercion that actually changes the underlying value?
Lifting to the ArrayList of something was fixed by making it invariant. Similarly then, is taking the address of something also invariant?

If anyone knows or finds out the answer to these before I do, through experimentation or reading up on Java, please post about it in the forum!